Search for: All records

Program verification and synthesis frameworks that allow one to customize the language in which one is interested typically require the user to provide a formally defined semantics for the language. Because writing a formal semantics can be a daunting and error-prone task, this requirement stands in the way of such frameworks being adopted by non-expert users. We present an algorithm that can automatically synthesize inductively defined syntax-directed semantics when given (i) a grammar describing the syntax of a language and (ii) an executable (closed-box) interpreter for computing the semantics of programs in the language of the grammar. Our algorithm synthesizes the semantics in the form of Constrained-Horn Clauses (CHCs), a natural, extensible, and formal logical framework for specifying inductively defined relations that has recently received widespread adoption in program verification and synthesis. The key innovation of our synthesis algorithm is a Counterexample-Guided Synthesis (CEGIS) approach that breaks the hard problem of synthesizing a set of constrained Horn clauses into small, tractable expression-synthesis problems that can be dispatched to existing SyGuS synthesizers. Our tool Synantic synthesized inductively-defined formal semantics from 14 interpreters for languages used in program-synthesis applications. When synthesizing formal semantics for one of our benchmarks, Synantic unveiled an inconsistency in the semantics computed by the interpreter for a language of regular expressions; fixing the inconsistency resulted in a more efficient semantics and, for some cases, in a 1.2x speedup for a synthesizer solving synthesis problems over such a language. 

Abstract The Hippo pathway effectors Yes-associated protein 1 (YAP) and its homolog TAZ are transcriptional coactivators that control gene expression by binding to TEA domain (TEAD) family transcription factors. The YAP/TAZ–TEAD complex is a key regulator of cancer-specific transcriptional programs, which promote tumor progression in diverse types of cancer, including breast cancer. Despite intensive efforts, the YAP/TAZ–TEAD complex in cancer has remained largely undruggable due to an incomplete mechanistic understanding. Here, we report that nuclear phosphoinositides function as cofactors that mediate the binding of YAP/TAZ to TEADs. The enzymatic products of phosphoinositide kinases PIPKIα and IPMK, including phosphatidylinositol 4,5-bisphosphate (PI(4,5)P₂) and phosphatidylinositol 3,4,5-trisphosphate (P(I3,4,5)P₃), bridge the binding of YAP/TAZ to TEAD. Inhibiting these kinases or the association of YAP/TAZ with PI(4,5)P₂and PI(3,4,5)P₃attenuates YAP/TAZ interaction with the TEADs, the expression of YAP/TAZ target genes, and breast cancer cell motility. Although we could not conclusively exclude the possibility that other enzymatic products of IPMK such as inositol phosphates play a role in the mechanism, our results point to a previously unrecognized role of nuclear phosphoinositide signaling in control of YAP/TAZ activity and implicate this pathway as a potential therapeutic target in YAP/TAZ-driven breast cancer. 

Abstract We started a survey with CHARA/MIRC-X and VLTI/GRAVITY to search for low-mass companions orbiting individual components of intermediate-mass binary systems. With the incredible precision of these instruments, we can detect astrometric “wobbles” from companions down to a few tens of microarcseconds. This allows us to detect any previously unseen triple systems in our list of binaries. We present the orbits of 12 companions around early F- to B-type binaries, 9 of which are new detections and 3 of which are first astrometric detections of known radial velocity (RV) companions. The masses of these newly detected components range from 0.45 to 1.3 M ⊙ . Our orbits constrain these systems to a high astrometric precision, with median residuals to the orbital fit of 20–50 μ as in most cases. For seven of these systems we include newly obtained RV data, which help us to identify the system configuration and to solve for masses of individual components in some cases. Although additional RV measurements are needed to break degeneracy in the mutual inclination, we find that the majority of these inner triples are not well aligned with the wide binary orbit. This hints that higher-mass triples are more misaligned compared to solar and lower-mass triples, though a thorough study of survey biases is needed. We show that the ARMADA survey is extremely successful at uncovering previously unseen companions in binaries. This method will be used in upcoming papers to constrain companion demographics in intermediate-mass binary systems down to the planetary-mass regime. 

We present a new polarimetric mode for the MIRC-X 6-telescope beam combiner at CHARA. Utilizing the extensive u - v coverage afforded by CHARA this mode will be able to resolve and constrain scattered light in environs at milliarcsecond separations of target stars, a largely unexplored parameter space to-date in astronomy. Notably, this upgrade will allow for the investigation of the scattering properties of the inner dust wall at the sublimation radius of Herbig Ae/Be star disks, dust shells surrounding evolved stars, and gas-rich disks around Be stars. Our design adds a series of rotating half-wave plates, achromatic across J- and H-bands, and a polarizing beamsplitter into the MIRC-X beam path. In this work, we also preview on-sky observations, discussing ongoing work calibrating instrumental polarization effects in the CHARA beam path as well as upgrades to the MIRC-X data reduction pipeline. 

When scientists disseminate their work to the general public, excessive use of jargon should be avoided because if too much technical language is used, the message is not effectively conveyed. However, determining which words are jargon and how much jargon is too much is a difficult task, partly because it can be challenging to know which terms the general public knows, and partly that it can be challenging to ensure scientific accuracy while avoiding esoteric terminology. To help address this issue, we have written an R script that an author can use to quantify the amount of scientific jargon in any written piece and make appropriate edits based on the target audience.